FDL - Nuprl Lemma : es-real-monotonicity

Nuprl Lemma : es-real-monotonicity

P, Q:(ES{i}

{i'}).
(

es:ES{i}. P(es)

Q(es))

es-real{i:l}(es.P(es))

es-real{i:l}(es.Q(es))

Definitions t T, P Q, x:A. B(x), ES, f(a), x(s), x. t(x), R ||- es.P(es), x:A. B(x), x:A B(x), es.P(es), Type, , x:AB(x)

Lemmas es-real wf, R-realizes wf, event system wf, R-implies-rule